Nuprl Lemma : scheme-realizes_wf
11,40
postcript
pdf
S
:RealizerScheme{i:l},
P
:(ES{i}
{i}). scheme-realizes{i:l}(
S
;
es
.
P
(
es
))
{i''}
latex
Definitions
ES
,
t
T
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
R
||-
es
.
P
(
es
)
,
Namer(
n
;
Id_list
)
,
Type
,
x
:
A
B
(
x
)
,
,
let
x
,
y
,
z
=
a
in
t
(
x
;
y
;
z
)
,
x
:
A
B
(
x
)
,
,
Id
,
type
List
,
Realizer
,
S
|-
es
.
P
(
es
)
,
RealizerScheme{i:l}()
Lemmas
Namer
wf
,
R-realizes
wf
origin
S:RealizerScheme{i:l}, P:(ES{i}
{i}). scheme-realizes{i:l}(S; es.P(es)) 
{i''} S:RealizerScheme{i:l}, P:(ES{i}{i}). scheme-realizes{i:l}(S; es.P(es)) {i''} T
x. t(x)x:A. B(x)B(x)
B(x)